H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 1.795 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ IFR

mainModule Main

((properFraction :: Float -> (Int,Float)) :: Float -> (Int,Float))

module Main where

import qualified Prelude

If Reductions:
The following If expression

if primGEqNatS x y then Succ (primDivNatS (primMinusNatS x y) (Succ y)) else Zero

is transformed to

primDivNatS0 x y True = Succ (primDivNatS (primMinusNatS x y) (Succ y))

primDivNatS0 x y False = Zero

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

mainModule Main

((properFraction :: Float -> (Int,Float)) :: Float -> (Int,Float))

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern

frac@(Float vv vw)

is replaced by the following term

Float vv vw

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule Main

((properFraction :: Float -> (Int,Float)) :: Float -> (Int,Float))

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

mainModule Main

((properFraction :: Float -> (Int,Float)) :: Float -> (Int,Float))

module Main where

import qualified Prelude

Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

mainModule Main

(properFraction :: Float -> (Int,Float))

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="properFraction",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="properFraction wv3",fontsize=16,color="black",shape="triangle"];3 -> 4[label="",style="solid", color="black", weight=3];
4[label="floatProperFractionFloat wv3",fontsize=16,color="burlywood",shape="box"];344[label="wv3/Float wv30 wv31",fontsize=10,color="white",style="solid",shape="box"];4 -> 344[label="",style="solid", color="burlywood", weight=9];
344 -> 5[label="",style="solid", color="burlywood", weight=3];
5[label="floatProperFractionFloat (Float wv30 wv31)",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="(fromInt (wv30 `quot` wv31),Float wv30 wv31 - fromInt (wv30 `quot` wv31))",fontsize=16,color="green",shape="box"];6 -> 7[label="",style="dashed", color="green", weight=3];
6 -> 8[label="",style="dashed", color="green", weight=3];
7[label="fromInt (wv30 `quot` wv31)",fontsize=16,color="black",shape="box"];7 -> 9[label="",style="solid", color="black", weight=3];
8[label="Float wv30 wv31 - fromInt (wv30 `quot` wv31)",fontsize=16,color="black",shape="box"];8 -> 10[label="",style="solid", color="black", weight=3];
9[label="wv30 `quot` wv31",fontsize=16,color="black",shape="triangle"];9 -> 11[label="",style="solid", color="black", weight=3];
10 -> 12[label="",style="dashed", color="red", weight=0];
10[label="primMinusFloat (Float wv30 wv31) (fromInt (wv30 `quot` wv31))",fontsize=16,color="magenta"];10 -> 13[label="",style="dashed", color="magenta", weight=3];
11[label="primQuotInt wv30 wv31",fontsize=16,color="burlywood",shape="box"];346[label="wv30/Pos wv300",fontsize=10,color="white",style="solid",shape="box"];11 -> 346[label="",style="solid", color="burlywood", weight=9];
346 -> 14[label="",style="solid", color="burlywood", weight=3];
347[label="wv30/Neg wv300",fontsize=10,color="white",style="solid",shape="box"];11 -> 347[label="",style="solid", color="burlywood", weight=9];
347 -> 15[label="",style="solid", color="burlywood", weight=3];
13 -> 9[label="",style="dashed", color="red", weight=0];
13[label="wv30 `quot` wv31",fontsize=16,color="magenta"];12[label="primMinusFloat (Float wv30 wv31) (fromInt wv4)",fontsize=16,color="black",shape="triangle"];12 -> 16[label="",style="solid", color="black", weight=3];
14[label="primQuotInt (Pos wv300) wv31",fontsize=16,color="burlywood",shape="box"];349[label="wv31/Pos wv310",fontsize=10,color="white",style="solid",shape="box"];14 -> 349[label="",style="solid", color="burlywood", weight=9];
349 -> 17[label="",style="solid", color="burlywood", weight=3];
350[label="wv31/Neg wv310",fontsize=10,color="white",style="solid",shape="box"];14 -> 350[label="",style="solid", color="burlywood", weight=9];
350 -> 18[label="",style="solid", color="burlywood", weight=3];
15[label="primQuotInt (Neg wv300) wv31",fontsize=16,color="burlywood",shape="box"];351[label="wv31/Pos wv310",fontsize=10,color="white",style="solid",shape="box"];15 -> 351[label="",style="solid", color="burlywood", weight=9];
351 -> 19[label="",style="solid", color="burlywood", weight=3];
352[label="wv31/Neg wv310",fontsize=10,color="white",style="solid",shape="box"];15 -> 352[label="",style="solid", color="burlywood", weight=9];
352 -> 20[label="",style="solid", color="burlywood", weight=3];
16[label="primMinusFloat (Float wv30 wv31) (primIntToFloat wv4)",fontsize=16,color="black",shape="box"];16 -> 21[label="",style="solid", color="black", weight=3];
17[label="primQuotInt (Pos wv300) (Pos wv310)",fontsize=16,color="burlywood",shape="box"];353[label="wv310/Succ wv3100",fontsize=10,color="white",style="solid",shape="box"];17 -> 353[label="",style="solid", color="burlywood", weight=9];
353 -> 22[label="",style="solid", color="burlywood", weight=3];
354[label="wv310/Zero",fontsize=10,color="white",style="solid",shape="box"];17 -> 354[label="",style="solid", color="burlywood", weight=9];
354 -> 23[label="",style="solid", color="burlywood", weight=3];
18[label="primQuotInt (Pos wv300) (Neg wv310)",fontsize=16,color="burlywood",shape="box"];355[label="wv310/Succ wv3100",fontsize=10,color="white",style="solid",shape="box"];18 -> 355[label="",style="solid", color="burlywood", weight=9];
355 -> 24[label="",style="solid", color="burlywood", weight=3];
356[label="wv310/Zero",fontsize=10,color="white",style="solid",shape="box"];18 -> 356[label="",style="solid", color="burlywood", weight=9];
356 -> 25[label="",style="solid", color="burlywood", weight=3];
19[label="primQuotInt (Neg wv300) (Pos wv310)",fontsize=16,color="burlywood",shape="box"];357[label="wv310/Succ wv3100",fontsize=10,color="white",style="solid",shape="box"];19 -> 357[label="",style="solid", color="burlywood", weight=9];
357 -> 26[label="",style="solid", color="burlywood", weight=3];
358[label="wv310/Zero",fontsize=10,color="white",style="solid",shape="box"];19 -> 358[label="",style="solid", color="burlywood", weight=9];
358 -> 27[label="",style="solid", color="burlywood", weight=3];
20[label="primQuotInt (Neg wv300) (Neg wv310)",fontsize=16,color="burlywood",shape="box"];359[label="wv310/Succ wv3100",fontsize=10,color="white",style="solid",shape="box"];20 -> 359[label="",style="solid", color="burlywood", weight=9];
359 -> 28[label="",style="solid", color="burlywood", weight=3];
360[label="wv310/Zero",fontsize=10,color="white",style="solid",shape="box"];20 -> 360[label="",style="solid", color="burlywood", weight=9];
360 -> 29[label="",style="solid", color="burlywood", weight=3];
21[label="primMinusFloat (Float wv30 wv31) (Float wv4 (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];21 -> 30[label="",style="solid", color="black", weight=3];
22[label="primQuotInt (Pos wv300) (Pos (Succ wv3100))",fontsize=16,color="black",shape="box"];22 -> 31[label="",style="solid", color="black", weight=3];
23[label="primQuotInt (Pos wv300) (Pos Zero)",fontsize=16,color="black",shape="box"];23 -> 32[label="",style="solid", color="black", weight=3];
24[label="primQuotInt (Pos wv300) (Neg (Succ wv3100))",fontsize=16,color="black",shape="box"];24 -> 33[label="",style="solid", color="black", weight=3];
25[label="primQuotInt (Pos wv300) (Neg Zero)",fontsize=16,color="black",shape="box"];25 -> 34[label="",style="solid", color="black", weight=3];
26[label="primQuotInt (Neg wv300) (Pos (Succ wv3100))",fontsize=16,color="black",shape="box"];26 -> 35[label="",style="solid", color="black", weight=3];
27[label="primQuotInt (Neg wv300) (Pos Zero)",fontsize=16,color="black",shape="box"];27 -> 36[label="",style="solid", color="black", weight=3];
28[label="primQuotInt (Neg wv300) (Neg (Succ wv3100))",fontsize=16,color="black",shape="box"];28 -> 37[label="",style="solid", color="black", weight=3];
29[label="primQuotInt (Neg wv300) (Neg Zero)",fontsize=16,color="black",shape="box"];29 -> 38[label="",style="solid", color="black", weight=3];
30[label="Float (wv30 - wv4) (wv31 * Pos (Succ Zero))",fontsize=16,color="green",shape="box"];30 -> 39[label="",style="dashed", color="green", weight=3];
30 -> 40[label="",style="dashed", color="green", weight=3];
31[label="Pos (primDivNatS wv300 (Succ wv3100))",fontsize=16,color="green",shape="box"];31 -> 41[label="",style="dashed", color="green", weight=3];
32[label="error []",fontsize=16,color="black",shape="triangle"];32 -> 42[label="",style="solid", color="black", weight=3];
33[label="Neg (primDivNatS wv300 (Succ wv3100))",fontsize=16,color="green",shape="box"];33 -> 43[label="",style="dashed", color="green", weight=3];
34 -> 32[label="",style="dashed", color="red", weight=0];
34[label="error []",fontsize=16,color="magenta"];35[label="Neg (primDivNatS wv300 (Succ wv3100))",fontsize=16,color="green",shape="box"];35 -> 44[label="",style="dashed", color="green", weight=3];
36 -> 32[label="",style="dashed", color="red", weight=0];
36[label="error []",fontsize=16,color="magenta"];37[label="Pos (primDivNatS wv300 (Succ wv3100))",fontsize=16,color="green",shape="box"];37 -> 45[label="",style="dashed", color="green", weight=3];
38 -> 32[label="",style="dashed", color="red", weight=0];
38[label="error []",fontsize=16,color="magenta"];39[label="wv30 - wv4",fontsize=16,color="black",shape="box"];39 -> 46[label="",style="solid", color="black", weight=3];
40[label="wv31 * Pos (Succ Zero)",fontsize=16,color="black",shape="box"];40 -> 47[label="",style="solid", color="black", weight=3];
41[label="primDivNatS wv300 (Succ wv3100)",fontsize=16,color="burlywood",shape="triangle"];364[label="wv300/Succ wv3000",fontsize=10,color="white",style="solid",shape="box"];41 -> 364[label="",style="solid", color="burlywood", weight=9];
364 -> 48[label="",style="solid", color="burlywood", weight=3];
365[label="wv300/Zero",fontsize=10,color="white",style="solid",shape="box"];41 -> 365[label="",style="solid", color="burlywood", weight=9];
365 -> 49[label="",style="solid", color="burlywood", weight=3];
42[label="error []",fontsize=16,color="red",shape="box"];43 -> 41[label="",style="dashed", color="red", weight=0];
43[label="primDivNatS wv300 (Succ wv3100)",fontsize=16,color="magenta"];43 -> 50[label="",style="dashed", color="magenta", weight=3];
44 -> 41[label="",style="dashed", color="red", weight=0];
44[label="primDivNatS wv300 (Succ wv3100)",fontsize=16,color="magenta"];44 -> 51[label="",style="dashed", color="magenta", weight=3];
45 -> 41[label="",style="dashed", color="red", weight=0];
45[label="primDivNatS wv300 (Succ wv3100)",fontsize=16,color="magenta"];45 -> 52[label="",style="dashed", color="magenta", weight=3];
45 -> 53[label="",style="dashed", color="magenta", weight=3];
46[label="primMinusInt wv30 wv4",fontsize=16,color="burlywood",shape="box"];369[label="wv30/Pos wv300",fontsize=10,color="white",style="solid",shape="box"];46 -> 369[label="",style="solid", color="burlywood", weight=9];
369 -> 54[label="",style="solid", color="burlywood", weight=3];
370[label="wv30/Neg wv300",fontsize=10,color="white",style="solid",shape="box"];46 -> 370[label="",style="solid", color="burlywood", weight=9];
370 -> 55[label="",style="solid", color="burlywood", weight=3];
47[label="primMulInt wv31 (Pos (Succ Zero))",fontsize=16,color="burlywood",shape="box"];371[label="wv31/Pos wv310",fontsize=10,color="white",style="solid",shape="box"];47 -> 371[label="",style="solid", color="burlywood", weight=9];
371 -> 56[label="",style="solid", color="burlywood", weight=3];
372[label="wv31/Neg wv310",fontsize=10,color="white",style="solid",shape="box"];47 -> 372[label="",style="solid", color="burlywood", weight=9];
372 -> 57[label="",style="solid", color="burlywood", weight=3];
48[label="primDivNatS (Succ wv3000) (Succ wv3100)",fontsize=16,color="black",shape="box"];48 -> 58[label="",style="solid", color="black", weight=3];
49[label="primDivNatS Zero (Succ wv3100)",fontsize=16,color="black",shape="box"];49 -> 59[label="",style="solid", color="black", weight=3];
50[label="wv3100",fontsize=16,color="green",shape="box"];51[label="wv300",fontsize=16,color="green",shape="box"];52[label="wv3100",fontsize=16,color="green",shape="box"];53[label="wv300",fontsize=16,color="green",shape="box"];54[label="primMinusInt (Pos wv300) wv4",fontsize=16,color="burlywood",shape="box"];373[label="wv4/Pos wv40",fontsize=10,color="white",style="solid",shape="box"];54 -> 373[label="",style="solid", color="burlywood", weight=9];
373 -> 60[label="",style="solid", color="burlywood", weight=3];
374[label="wv4/Neg wv40",fontsize=10,color="white",style="solid",shape="box"];54 -> 374[label="",style="solid", color="burlywood", weight=9];
374 -> 61[label="",style="solid", color="burlywood", weight=3];
55[label="primMinusInt (Neg wv300) wv4",fontsize=16,color="burlywood",shape="box"];375[label="wv4/Pos wv40",fontsize=10,color="white",style="solid",shape="box"];55 -> 375[label="",style="solid", color="burlywood", weight=9];
375 -> 62[label="",style="solid", color="burlywood", weight=3];
376[label="wv4/Neg wv40",fontsize=10,color="white",style="solid",shape="box"];55 -> 376[label="",style="solid", color="burlywood", weight=9];
376 -> 63[label="",style="solid", color="burlywood", weight=3];
56[label="primMulInt (Pos wv310) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];56 -> 64[label="",style="solid", color="black", weight=3];
57[label="primMulInt (Neg wv310) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];57 -> 65[label="",style="solid", color="black", weight=3];
58[label="primDivNatS0 wv3000 wv3100 (primGEqNatS wv3000 wv3100)",fontsize=16,color="burlywood",shape="box"];377[label="wv3000/Succ wv30000",fontsize=10,color="white",style="solid",shape="box"];58 -> 377[label="",style="solid", color="burlywood", weight=9];
377 -> 66[label="",style="solid", color="burlywood", weight=3];
378[label="wv3000/Zero",fontsize=10,color="white",style="solid",shape="box"];58 -> 378[label="",style="solid", color="burlywood", weight=9];
378 -> 67[label="",style="solid", color="burlywood", weight=3];
59[label="Zero",fontsize=16,color="green",shape="box"];60[label="primMinusInt (Pos wv300) (Pos wv40)",fontsize=16,color="black",shape="box"];60 -> 68[label="",style="solid", color="black", weight=3];
61[label="primMinusInt (Pos wv300) (Neg wv40)",fontsize=16,color="black",shape="box"];61 -> 69[label="",style="solid", color="black", weight=3];
62[label="primMinusInt (Neg wv300) (Pos wv40)",fontsize=16,color="black",shape="box"];62 -> 70[label="",style="solid", color="black", weight=3];
63[label="primMinusInt (Neg wv300) (Neg wv40)",fontsize=16,color="black",shape="box"];63 -> 71[label="",style="solid", color="black", weight=3];
64[label="Pos (primMulNat wv310 (Succ Zero))",fontsize=16,color="green",shape="box"];64 -> 72[label="",style="dashed", color="green", weight=3];
65[label="Neg (primMulNat wv310 (Succ Zero))",fontsize=16,color="green",shape="box"];65 -> 73[label="",style="dashed", color="green", weight=3];
66[label="primDivNatS0 (Succ wv30000) wv3100 (primGEqNatS (Succ wv30000) wv3100)",fontsize=16,color="burlywood",shape="box"];379[label="wv3100/Succ wv31000",fontsize=10,color="white",style="solid",shape="box"];66 -> 379[label="",style="solid", color="burlywood", weight=9];
379 -> 74[label="",style="solid", color="burlywood", weight=3];
380[label="wv3100/Zero",fontsize=10,color="white",style="solid",shape="box"];66 -> 380[label="",style="solid", color="burlywood", weight=9];
380 -> 75[label="",style="solid", color="burlywood", weight=3];
67[label="primDivNatS0 Zero wv3100 (primGEqNatS Zero wv3100)",fontsize=16,color="burlywood",shape="box"];381[label="wv3100/Succ wv31000",fontsize=10,color="white",style="solid",shape="box"];67 -> 381[label="",style="solid", color="burlywood", weight=9];
381 -> 76[label="",style="solid", color="burlywood", weight=3];
382[label="wv3100/Zero",fontsize=10,color="white",style="solid",shape="box"];67 -> 382[label="",style="solid", color="burlywood", weight=9];
382 -> 77[label="",style="solid", color="burlywood", weight=3];
68[label="primMinusNat wv300 wv40",fontsize=16,color="burlywood",shape="triangle"];383[label="wv300/Succ wv3000",fontsize=10,color="white",style="solid",shape="box"];68 -> 383[label="",style="solid", color="burlywood", weight=9];
383 -> 78[label="",style="solid", color="burlywood", weight=3];
384[label="wv300/Zero",fontsize=10,color="white",style="solid",shape="box"];68 -> 384[label="",style="solid", color="burlywood", weight=9];
384 -> 79[label="",style="solid", color="burlywood", weight=3];
69[label="Pos (primPlusNat wv300 wv40)",fontsize=16,color="green",shape="box"];69 -> 80[label="",style="dashed", color="green", weight=3];
70[label="Neg (primPlusNat wv300 wv40)",fontsize=16,color="green",shape="box"];70 -> 81[label="",style="dashed", color="green", weight=3];
71 -> 68[label="",style="dashed", color="red", weight=0];
71[label="primMinusNat wv40 wv300",fontsize=16,color="magenta"];71 -> 82[label="",style="dashed", color="magenta", weight=3];
71 -> 83[label="",style="dashed", color="magenta", weight=3];
72[label="primMulNat wv310 (Succ Zero)",fontsize=16,color="burlywood",shape="triangle"];386[label="wv310/Succ wv3100",fontsize=10,color="white",style="solid",shape="box"];72 -> 386[label="",style="solid", color="burlywood", weight=9];
386 -> 84[label="",style="solid", color="burlywood", weight=3];
387[label="wv310/Zero",fontsize=10,color="white",style="solid",shape="box"];72 -> 387[label="",style="solid", color="burlywood", weight=9];
387 -> 85[label="",style="solid", color="burlywood", weight=3];
73 -> 72[label="",style="dashed", color="red", weight=0];
73[label="primMulNat wv310 (Succ Zero)",fontsize=16,color="magenta"];73 -> 86[label="",style="dashed", color="magenta", weight=3];
74[label="primDivNatS0 (Succ wv30000) (Succ wv31000) (primGEqNatS (Succ wv30000) (Succ wv31000))",fontsize=16,color="black",shape="box"];74 -> 87[label="",style="solid", color="black", weight=3];
75[label="primDivNatS0 (Succ wv30000) Zero (primGEqNatS (Succ wv30000) Zero)",fontsize=16,color="black",shape="box"];75 -> 88[label="",style="solid", color="black", weight=3];
76[label="primDivNatS0 Zero (Succ wv31000) (primGEqNatS Zero (Succ wv31000))",fontsize=16,color="black",shape="box"];76 -> 89[label="",style="solid", color="black", weight=3];
77[label="primDivNatS0 Zero Zero (primGEqNatS Zero Zero)",fontsize=16,color="black",shape="box"];77 -> 90[label="",style="solid", color="black", weight=3];
78[label="primMinusNat (Succ wv3000) wv40",fontsize=16,color="burlywood",shape="box"];389[label="wv40/Succ wv400",fontsize=10,color="white",style="solid",shape="box"];78 -> 389[label="",style="solid", color="burlywood", weight=9];
389 -> 91[label="",style="solid", color="burlywood", weight=3];
390[label="wv40/Zero",fontsize=10,color="white",style="solid",shape="box"];78 -> 390[label="",style="solid", color="burlywood", weight=9];
390 -> 92[label="",style="solid", color="burlywood", weight=3];
79[label="primMinusNat Zero wv40",fontsize=16,color="burlywood",shape="box"];391[label="wv40/Succ wv400",fontsize=10,color="white",style="solid",shape="box"];79 -> 391[label="",style="solid", color="burlywood", weight=9];
391 -> 93[label="",style="solid", color="burlywood", weight=3];
392[label="wv40/Zero",fontsize=10,color="white",style="solid",shape="box"];79 -> 392[label="",style="solid", color="burlywood", weight=9];
392 -> 94[label="",style="solid", color="burlywood", weight=3];
80[label="primPlusNat wv300 wv40",fontsize=16,color="burlywood",shape="triangle"];393[label="wv300/Succ wv3000",fontsize=10,color="white",style="solid",shape="box"];80 -> 393[label="",style="solid", color="burlywood", weight=9];
393 -> 95[label="",style="solid", color="burlywood", weight=3];
394[label="wv300/Zero",fontsize=10,color="white",style="solid",shape="box"];80 -> 394[label="",style="solid", color="burlywood", weight=9];
394 -> 96[label="",style="solid", color="burlywood", weight=3];
81 -> 80[label="",style="dashed", color="red", weight=0];
81[label="primPlusNat wv300 wv40",fontsize=16,color="magenta"];81 -> 97[label="",style="dashed", color="magenta", weight=3];
81 -> 98[label="",style="dashed", color="magenta", weight=3];
82[label="wv40",fontsize=16,color="green",shape="box"];83[label="wv300",fontsize=16,color="green",shape="box"];84[label="primMulNat (Succ wv3100) (Succ Zero)",fontsize=16,color="black",shape="box"];84 -> 99[label="",style="solid", color="black", weight=3];
85[label="primMulNat Zero (Succ Zero)",fontsize=16,color="black",shape="box"];85 -> 100[label="",style="solid", color="black", weight=3];
86[label="wv310",fontsize=16,color="green",shape="box"];87 -> 281[label="",style="dashed", color="red", weight=0];
87[label="primDivNatS0 (Succ wv30000) (Succ wv31000) (primGEqNatS wv30000 wv31000)",fontsize=16,color="magenta"];87 -> 282[label="",style="dashed", color="magenta", weight=3];
87 -> 283[label="",style="dashed", color="magenta", weight=3];
87 -> 284[label="",style="dashed", color="magenta", weight=3];
87 -> 285[label="",style="dashed", color="magenta", weight=3];
88[label="primDivNatS0 (Succ wv30000) Zero True",fontsize=16,color="black",shape="box"];88 -> 103[label="",style="solid", color="black", weight=3];
89[label="primDivNatS0 Zero (Succ wv31000) False",fontsize=16,color="black",shape="box"];89 -> 104[label="",style="solid", color="black", weight=3];
90[label="primDivNatS0 Zero Zero True",fontsize=16,color="black",shape="box"];90 -> 105[label="",style="solid", color="black", weight=3];
91[label="primMinusNat (Succ wv3000) (Succ wv400)",fontsize=16,color="black",shape="box"];91 -> 106[label="",style="solid", color="black", weight=3];
92[label="primMinusNat (Succ wv3000) Zero",fontsize=16,color="black",shape="box"];92 -> 107[label="",style="solid", color="black", weight=3];
93[label="primMinusNat Zero (Succ wv400)",fontsize=16,color="black",shape="box"];93 -> 108[label="",style="solid", color="black", weight=3];
94[label="primMinusNat Zero Zero",fontsize=16,color="black",shape="box"];94 -> 109[label="",style="solid", color="black", weight=3];
95[label="primPlusNat (Succ wv3000) wv40",fontsize=16,color="burlywood",shape="box"];397[label="wv40/Succ wv400",fontsize=10,color="white",style="solid",shape="box"];95 -> 397[label="",style="solid", color="burlywood", weight=9];
397 -> 110[label="",style="solid", color="burlywood", weight=3];
398[label="wv40/Zero",fontsize=10,color="white",style="solid",shape="box"];95 -> 398[label="",style="solid", color="burlywood", weight=9];
398 -> 111[label="",style="solid", color="burlywood", weight=3];
96[label="primPlusNat Zero wv40",fontsize=16,color="burlywood",shape="box"];399[label="wv40/Succ wv400",fontsize=10,color="white",style="solid",shape="box"];96 -> 399[label="",style="solid", color="burlywood", weight=9];
399 -> 112[label="",style="solid", color="burlywood", weight=3];
400[label="wv40/Zero",fontsize=10,color="white",style="solid",shape="box"];96 -> 400[label="",style="solid", color="burlywood", weight=9];
400 -> 113[label="",style="solid", color="burlywood", weight=3];
97[label="wv300",fontsize=16,color="green",shape="box"];98[label="wv40",fontsize=16,color="green",shape="box"];99 -> 80[label="",style="dashed", color="red", weight=0];
99[label="primPlusNat (primMulNat wv3100 (Succ Zero)) (Succ Zero)",fontsize=16,color="magenta"];99 -> 114[label="",style="dashed", color="magenta", weight=3];
99 -> 115[label="",style="dashed", color="magenta", weight=3];
100[label="Zero",fontsize=16,color="green",shape="box"];282[label="wv30000",fontsize=16,color="green",shape="box"];283[label="wv30000",fontsize=16,color="green",shape="box"];284[label="wv31000",fontsize=16,color="green",shape="box"];285[label="wv31000",fontsize=16,color="green",shape="box"];281[label="primDivNatS0 (Succ wv21) (Succ wv22) (primGEqNatS wv23 wv24)",fontsize=16,color="burlywood",shape="triangle"];402[label="wv23/Succ wv230",fontsize=10,color="white",style="solid",shape="box"];281 -> 402[label="",style="solid", color="burlywood", weight=9];
402 -> 314[label="",style="solid", color="burlywood", weight=3];
403[label="wv23/Zero",fontsize=10,color="white",style="solid",shape="box"];281 -> 403[label="",style="solid", color="burlywood", weight=9];
403 -> 315[label="",style="solid", color="burlywood", weight=3];
103[label="Succ (primDivNatS (primMinusNatS (Succ wv30000) Zero) (Succ Zero))",fontsize=16,color="green",shape="box"];103 -> 120[label="",style="dashed", color="green", weight=3];
104[label="Zero",fontsize=16,color="green",shape="box"];105[label="Succ (primDivNatS (primMinusNatS Zero Zero) (Succ Zero))",fontsize=16,color="green",shape="box"];105 -> 121[label="",style="dashed", color="green", weight=3];
106 -> 68[label="",style="dashed", color="red", weight=0];
106[label="primMinusNat wv3000 wv400",fontsize=16,color="magenta"];106 -> 122[label="",style="dashed", color="magenta", weight=3];
106 -> 123[label="",style="dashed", color="magenta", weight=3];
107[label="Pos (Succ wv3000)",fontsize=16,color="green",shape="box"];108[label="Neg (Succ wv400)",fontsize=16,color="green",shape="box"];109[label="Pos Zero",fontsize=16,color="green",shape="box"];110[label="primPlusNat (Succ wv3000) (Succ wv400)",fontsize=16,color="black",shape="box"];110 -> 124[label="",style="solid", color="black", weight=3];
111[label="primPlusNat (Succ wv3000) Zero",fontsize=16,color="black",shape="box"];111 -> 125[label="",style="solid", color="black", weight=3];
112[label="primPlusNat Zero (Succ wv400)",fontsize=16,color="black",shape="box"];112 -> 126[label="",style="solid", color="black", weight=3];
113[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="box"];113 -> 127[label="",style="solid", color="black", weight=3];
114 -> 72[label="",style="dashed", color="red", weight=0];
114[label="primMulNat wv3100 (Succ Zero)",fontsize=16,color="magenta"];114 -> 128[label="",style="dashed", color="magenta", weight=3];
115[label="Succ Zero",fontsize=16,color="green",shape="box"];314[label="primDivNatS0 (Succ wv21) (Succ wv22) (primGEqNatS (Succ wv230) wv24)",fontsize=16,color="burlywood",shape="box"];406[label="wv24/Succ wv240",fontsize=10,color="white",style="solid",shape="box"];314 -> 406[label="",style="solid", color="burlywood", weight=9];
406 -> 316[label="",style="solid", color="burlywood", weight=3];
407[label="wv24/Zero",fontsize=10,color="white",style="solid",shape="box"];314 -> 407[label="",style="solid", color="burlywood", weight=9];
407 -> 317[label="",style="solid", color="burlywood", weight=3];
315[label="primDivNatS0 (Succ wv21) (Succ wv22) (primGEqNatS Zero wv24)",fontsize=16,color="burlywood",shape="box"];408[label="wv24/Succ wv240",fontsize=10,color="white",style="solid",shape="box"];315 -> 408[label="",style="solid", color="burlywood", weight=9];
408 -> 318[label="",style="solid", color="burlywood", weight=3];
409[label="wv24/Zero",fontsize=10,color="white",style="solid",shape="box"];315 -> 409[label="",style="solid", color="burlywood", weight=9];
409 -> 319[label="",style="solid", color="burlywood", weight=3];
120 -> 41[label="",style="dashed", color="red", weight=0];
120[label="primDivNatS (primMinusNatS (Succ wv30000) Zero) (Succ Zero)",fontsize=16,color="magenta"];120 -> 133[label="",style="dashed", color="magenta", weight=3];
120 -> 134[label="",style="dashed", color="magenta", weight=3];
121 -> 41[label="",style="dashed", color="red", weight=0];
121[label="primDivNatS (primMinusNatS Zero Zero) (Succ Zero)",fontsize=16,color="magenta"];121 -> 135[label="",style="dashed", color="magenta", weight=3];
121 -> 136[label="",style="dashed", color="magenta", weight=3];
122[label="wv3000",fontsize=16,color="green",shape="box"];123[label="wv400",fontsize=16,color="green",shape="box"];124[label="Succ (Succ (primPlusNat wv3000 wv400))",fontsize=16,color="green",shape="box"];124 -> 137[label="",style="dashed", color="green", weight=3];
125[label="Succ wv3000",fontsize=16,color="green",shape="box"];126[label="Succ wv400",fontsize=16,color="green",shape="box"];127[label="Zero",fontsize=16,color="green",shape="box"];128[label="wv3100",fontsize=16,color="green",shape="box"];316[label="primDivNatS0 (Succ wv21) (Succ wv22) (primGEqNatS (Succ wv230) (Succ wv240))",fontsize=16,color="black",shape="box"];316 -> 320[label="",style="solid", color="black", weight=3];
317[label="primDivNatS0 (Succ wv21) (Succ wv22) (primGEqNatS (Succ wv230) Zero)",fontsize=16,color="black",shape="box"];317 -> 321[label="",style="solid", color="black", weight=3];
318[label="primDivNatS0 (Succ wv21) (Succ wv22) (primGEqNatS Zero (Succ wv240))",fontsize=16,color="black",shape="box"];318 -> 322[label="",style="solid", color="black", weight=3];
319[label="primDivNatS0 (Succ wv21) (Succ wv22) (primGEqNatS Zero Zero)",fontsize=16,color="black",shape="box"];319 -> 323[label="",style="solid", color="black", weight=3];
133[label="Zero",fontsize=16,color="green",shape="box"];134[label="primMinusNatS (Succ wv30000) Zero",fontsize=16,color="black",shape="triangle"];134 -> 143[label="",style="solid", color="black", weight=3];
135[label="Zero",fontsize=16,color="green",shape="box"];136[label="primMinusNatS Zero Zero",fontsize=16,color="black",shape="triangle"];136 -> 144[label="",style="solid", color="black", weight=3];
137 -> 80[label="",style="dashed", color="red", weight=0];
137[label="primPlusNat wv3000 wv400",fontsize=16,color="magenta"];137 -> 145[label="",style="dashed", color="magenta", weight=3];
137 -> 146[label="",style="dashed", color="magenta", weight=3];
320 -> 281[label="",style="dashed", color="red", weight=0];
320[label="primDivNatS0 (Succ wv21) (Succ wv22) (primGEqNatS wv230 wv240)",fontsize=16,color="magenta"];320 -> 324[label="",style="dashed", color="magenta", weight=3];
320 -> 325[label="",style="dashed", color="magenta", weight=3];
321[label="primDivNatS0 (Succ wv21) (Succ wv22) True",fontsize=16,color="black",shape="triangle"];321 -> 326[label="",style="solid", color="black", weight=3];
322[label="primDivNatS0 (Succ wv21) (Succ wv22) False",fontsize=16,color="black",shape="box"];322 -> 327[label="",style="solid", color="black", weight=3];
323 -> 321[label="",style="dashed", color="red", weight=0];
323[label="primDivNatS0 (Succ wv21) (Succ wv22) True",fontsize=16,color="magenta"];143[label="Succ wv30000",fontsize=16,color="green",shape="box"];144[label="Zero",fontsize=16,color="green",shape="box"];145[label="wv3000",fontsize=16,color="green",shape="box"];146[label="wv400",fontsize=16,color="green",shape="box"];324[label="wv230",fontsize=16,color="green",shape="box"];325[label="wv240",fontsize=16,color="green",shape="box"];326[label="Succ (primDivNatS (primMinusNatS (Succ wv21) (Succ wv22)) (Succ (Succ wv22)))",fontsize=16,color="green",shape="box"];326 -> 328[label="",style="dashed", color="green", weight=3];
327[label="Zero",fontsize=16,color="green",shape="box"];328 -> 41[label="",style="dashed", color="red", weight=0];
328[label="primDivNatS (primMinusNatS (Succ wv21) (Succ wv22)) (Succ (Succ wv22))",fontsize=16,color="magenta"];328 -> 329[label="",style="dashed", color="magenta", weight=3];
328 -> 330[label="",style="dashed", color="magenta", weight=3];
329[label="Succ wv22",fontsize=16,color="green",shape="box"];330[label="primMinusNatS (Succ wv21) (Succ wv22)",fontsize=16,color="black",shape="box"];330 -> 331[label="",style="solid", color="black", weight=3];
331[label="primMinusNatS wv21 wv22",fontsize=16,color="burlywood",shape="triangle"];416[label="wv21/Succ wv210",fontsize=10,color="white",style="solid",shape="box"];331 -> 416[label="",style="solid", color="burlywood", weight=9];
416 -> 332[label="",style="solid", color="burlywood", weight=3];
417[label="wv21/Zero",fontsize=10,color="white",style="solid",shape="box"];331 -> 417[label="",style="solid", color="burlywood", weight=9];
417 -> 333[label="",style="solid", color="burlywood", weight=3];
332[label="primMinusNatS (Succ wv210) wv22",fontsize=16,color="burlywood",shape="box"];418[label="wv22/Succ wv220",fontsize=10,color="white",style="solid",shape="box"];332 -> 418[label="",style="solid", color="burlywood", weight=9];
418 -> 334[label="",style="solid", color="burlywood", weight=3];
419[label="wv22/Zero",fontsize=10,color="white",style="solid",shape="box"];332 -> 419[label="",style="solid", color="burlywood", weight=9];
419 -> 335[label="",style="solid", color="burlywood", weight=3];
333[label="primMinusNatS Zero wv22",fontsize=16,color="burlywood",shape="box"];420[label="wv22/Succ wv220",fontsize=10,color="white",style="solid",shape="box"];333 -> 420[label="",style="solid", color="burlywood", weight=9];
420 -> 336[label="",style="solid", color="burlywood", weight=3];
421[label="wv22/Zero",fontsize=10,color="white",style="solid",shape="box"];333 -> 421[label="",style="solid", color="burlywood", weight=9];
421 -> 337[label="",style="solid", color="burlywood", weight=3];
334[label="primMinusNatS (Succ wv210) (Succ wv220)",fontsize=16,color="black",shape="box"];334 -> 338[label="",style="solid", color="black", weight=3];
335[label="primMinusNatS (Succ wv210) Zero",fontsize=16,color="black",shape="box"];335 -> 339[label="",style="solid", color="black", weight=3];
336[label="primMinusNatS Zero (Succ wv220)",fontsize=16,color="black",shape="box"];336 -> 340[label="",style="solid", color="black", weight=3];
337[label="primMinusNatS Zero Zero",fontsize=16,color="black",shape="box"];337 -> 341[label="",style="solid", color="black", weight=3];
338 -> 331[label="",style="dashed", color="red", weight=0];
338[label="primMinusNatS wv210 wv220",fontsize=16,color="magenta"];338 -> 342[label="",style="dashed", color="magenta", weight=3];
338 -> 343[label="",style="dashed", color="magenta", weight=3];
339[label="Succ wv210",fontsize=16,color="green",shape="box"];340[label="Zero",fontsize=16,color="green",shape="box"];341[label="Zero",fontsize=16,color="green",shape="box"];342[label="wv210",fontsize=16,color="green",shape="box"];343[label="wv220",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(wv3000), Succ(wv400)) → new_primPlusNat(wv3000, wv400)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_primPlusNat(Succ(wv3000), Succ(wv400)) → new_primPlusNat(wv3000, wv400)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(wv3100)) → new_primMulNat(wv3100)

From the DPs we obtained the following set of size-change graphs:

new_primMulNat(Succ(wv3100)) → new_primMulNat(wv3100)
The graph contains the following edges 1 > 1

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                      ↳ QDP

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat(Succ(wv3000), Succ(wv400)) → new_primMinusNat(wv3000, wv400)

From the DPs we obtained the following set of size-change graphs:

new_primMinusNat(Succ(wv3000), Succ(wv400)) → new_primMinusNat(wv3000, wv400)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNatS(Succ(wv210), Succ(wv220)) → new_primMinusNatS(wv210, wv220)

From the DPs we obtained the following set of size-change graphs:

new_primMinusNatS(Succ(wv210), Succ(wv220)) → new_primMinusNatS(wv210, wv220)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(wv21, wv22, Zero, Zero) → new_primDivNatS00(wv21, wv22)
new_primDivNatS0(wv21, wv22, Succ(wv230), Succ(wv240)) → new_primDivNatS0(wv21, wv22, wv230, wv240)
new_primDivNatS00(wv21, wv22) → new_primDivNatS(new_primMinusNatS0(wv21, wv22), Succ(wv22))
new_primDivNatS(Succ(Succ(wv30000)), Succ(wv31000)) → new_primDivNatS0(wv30000, wv31000, wv30000, wv31000)
new_primDivNatS0(wv21, wv22, Succ(wv230), Zero) → new_primDivNatS(new_primMinusNatS0(wv21, wv22), Succ(wv22))
new_primDivNatS(Succ(Zero), Zero) → new_primDivNatS(new_primMinusNatS2, Zero)
new_primDivNatS(Succ(Succ(wv30000)), Zero) → new_primDivNatS(new_primMinusNatS1(wv30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(wv220)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS1(wv30000) → Succ(wv30000)
new_primMinusNatS0(Succ(wv210), Succ(wv220)) → new_primMinusNatS0(wv210, wv220)
new_primMinusNatS0(Succ(wv210), Zero) → Succ(wv210)
new_primMinusNatS2 → Zero

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS1(x0)
new_primMinusNatS2
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 1 less node.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                              ↳ UsableRulesProof

                            ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(wv30000)), Zero) → new_primDivNatS(new_primMinusNatS1(wv30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(wv220)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS1(wv30000) → Succ(wv30000)
new_primMinusNatS0(Succ(wv210), Succ(wv220)) → new_primMinusNatS0(wv210, wv220)
new_primMinusNatS0(Succ(wv210), Zero) → Succ(wv210)
new_primMinusNatS2 → Zero

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS1(x0)
new_primMinusNatS2
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                            ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(wv30000)), Zero) → new_primDivNatS(new_primMinusNatS1(wv30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS1(wv30000) → Succ(wv30000)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS1(x0)
new_primMinusNatS2
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS2
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Zero)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RuleRemovalProof

                            ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(wv30000)), Zero) → new_primDivNatS(new_primMinusNatS1(wv30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS1(wv30000) → Succ(wv30000)

The set Q consists of the following terms:

new_primMinusNatS1(x0)

We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

new_primDivNatS(Succ(Succ(wv30000)), Zero) → new_primDivNatS(new_primMinusNatS1(wv30000), Zero)

Strictly oriented rules of the TRS R:

new_primMinusNatS1(wv30000) → Succ(wv30000)

Used ordering: POLO with Polynomial interpretation [25]:

POL(Succ(x₁)) = 1 + 2·x₁
POL(Zero) = 0
POL(new_primDivNatS(x₁, x₂)) = x₁ + x₂
POL(new_primMinusNatS1(x₁)) = 2 + 2·x₁

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RuleRemovalProof

                                        ↳ QDP

                                          ↳ PisEmptyProof

                            ↳ QDP

Q DP problem:
P is empty.
R is empty.
The set Q consists of the following terms:

new_primMinusNatS1(x0)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(wv21, wv22, Zero, Zero) → new_primDivNatS00(wv21, wv22)
new_primDivNatS0(wv21, wv22, Succ(wv230), Succ(wv240)) → new_primDivNatS0(wv21, wv22, wv230, wv240)
new_primDivNatS(Succ(Succ(wv30000)), Succ(wv31000)) → new_primDivNatS0(wv30000, wv31000, wv30000, wv31000)
new_primDivNatS00(wv21, wv22) → new_primDivNatS(new_primMinusNatS0(wv21, wv22), Succ(wv22))
new_primDivNatS0(wv21, wv22, Succ(wv230), Zero) → new_primDivNatS(new_primMinusNatS0(wv21, wv22), Succ(wv22))

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(wv220)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS1(wv30000) → Succ(wv30000)
new_primMinusNatS0(Succ(wv210), Succ(wv220)) → new_primMinusNatS0(wv210, wv220)
new_primMinusNatS0(Succ(wv210), Zero) → Succ(wv210)
new_primMinusNatS2 → Zero

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS1(x0)
new_primMinusNatS2
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Zero)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(wv21, wv22, Zero, Zero) → new_primDivNatS00(wv21, wv22)
new_primDivNatS0(wv21, wv22, Succ(wv230), Succ(wv240)) → new_primDivNatS0(wv21, wv22, wv230, wv240)
new_primDivNatS(Succ(Succ(wv30000)), Succ(wv31000)) → new_primDivNatS0(wv30000, wv31000, wv30000, wv31000)
new_primDivNatS00(wv21, wv22) → new_primDivNatS(new_primMinusNatS0(wv21, wv22), Succ(wv22))
new_primDivNatS0(wv21, wv22, Succ(wv230), Zero) → new_primDivNatS(new_primMinusNatS0(wv21, wv22), Succ(wv22))

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(wv220)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(wv210), Succ(wv220)) → new_primMinusNatS0(wv210, wv220)
new_primMinusNatS0(Succ(wv210), Zero) → Succ(wv210)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS1(x0)
new_primMinusNatS2
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS1(x0)
new_primMinusNatS2

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(wv21, wv22, Zero, Zero) → new_primDivNatS00(wv21, wv22)
new_primDivNatS00(wv21, wv22) → new_primDivNatS(new_primMinusNatS0(wv21, wv22), Succ(wv22))
new_primDivNatS(Succ(Succ(wv30000)), Succ(wv31000)) → new_primDivNatS0(wv30000, wv31000, wv30000, wv31000)
new_primDivNatS0(wv21, wv22, Succ(wv230), Succ(wv240)) → new_primDivNatS0(wv21, wv22, wv230, wv240)
new_primDivNatS0(wv21, wv22, Succ(wv230), Zero) → new_primDivNatS(new_primMinusNatS0(wv21, wv22), Succ(wv22))

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(wv220)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(wv210), Succ(wv220)) → new_primMinusNatS0(wv210, wv220)
new_primMinusNatS0(Succ(wv210), Zero) → Succ(wv210)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_primDivNatS00(wv21, wv22) → new_primDivNatS(new_primMinusNatS0(wv21, wv22), Succ(wv22))
new_primDivNatS(Succ(Succ(wv30000)), Succ(wv31000)) → new_primDivNatS0(wv30000, wv31000, wv30000, wv31000)
new_primDivNatS0(wv21, wv22, Succ(wv230), Zero) → new_primDivNatS(new_primMinusNatS0(wv21, wv22), Succ(wv22))

The remaining pairs can at least be oriented weakly.

new_primDivNatS0(wv21, wv22, Zero, Zero) → new_primDivNatS00(wv21, wv22)
new_primDivNatS0(wv21, wv22, Succ(wv230), Succ(wv240)) → new_primDivNatS0(wv21, wv22, wv230, wv240)

Used ordering: Polynomial interpretation [25]:

POL(Succ(x₁)) = 1 + x₁
POL(Zero) = 0
POL(new_primDivNatS(x₁, x₂)) = x₁
POL(new_primDivNatS0(x₁, x₂, x₃, x₄)) = 1 + x₁
POL(new_primDivNatS00(x₁, x₂)) = 1 + x₁
POL(new_primMinusNatS0(x₁, x₂)) = x₁

The following usable rules [17] were oriented:

new_primMinusNatS0(Succ(wv210), Zero) → Succ(wv210)
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Zero, Succ(wv220)) → Zero
new_primMinusNatS0(Succ(wv210), Succ(wv220)) → new_primMinusNatS0(wv210, wv220)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ QDPOrderProof

                                        ↳ QDP

                                          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(wv21, wv22, Zero, Zero) → new_primDivNatS00(wv21, wv22)
new_primDivNatS0(wv21, wv22, Succ(wv230), Succ(wv240)) → new_primDivNatS0(wv21, wv22, wv230, wv240)

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(wv220)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(wv210), Succ(wv220)) → new_primMinusNatS0(wv210, wv220)
new_primMinusNatS0(Succ(wv210), Zero) → Succ(wv210)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ QDPOrderProof

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(wv21, wv22, Succ(wv230), Succ(wv240)) → new_primDivNatS0(wv21, wv22, wv230, wv240)

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(wv220)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(wv210), Succ(wv220)) → new_primMinusNatS0(wv210, wv220)
new_primMinusNatS0(Succ(wv210), Zero) → Succ(wv210)

The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Zero)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ QDPOrderProof

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ UsableRulesProof

                                                ↳ QDP

                                                  ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(wv21, wv22, Succ(wv230), Succ(wv240)) → new_primDivNatS0(wv21, wv22, wv230, wv240)

R is empty.
The set Q consists of the following terms:

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS0(Zero, Succ(x0))
new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Zero)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ QDPOrderProof

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ UsableRulesProof

                                                ↳ QDP

                                                  ↳ QReductionProof

                                                    ↳ QDP

                                                      ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(wv21, wv22, Succ(wv230), Succ(wv240)) → new_primDivNatS0(wv21, wv22, wv230, wv240)

From the DPs we obtained the following set of size-change graphs:

new_primDivNatS0(wv21, wv22, Succ(wv230), Succ(wv240)) → new_primDivNatS0(wv21, wv22, wv230, wv240)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4

primDivNatS0	x y True	= Succ (primDivNatS (primMinusNatS x y) (Succ y))
primDivNatS0	x y False	= Zero